Nuprl Lemma : add_mono_wrt_lt_rw
12,41
postcript
pdf
a
,
b
,
n
:
. {(
a
<
b
)
((
a
+
n
) < (
b
+
n
))}
latex
ProofTree
Definitions
{
T
}
Lemmas
add
mono
wrt
lt
origin
a, b, n:
. {(a < b) 
((a+n) < (b+n))}
a, b, n:. {(a < b) ((a+n) < (b+n))}